package kodkod.analysis;

import java.util.HashSet;

import kodkod.ast.*;

public class AllQDecls extends HashSet<Variable> {
	
	public AllQDecls(ComparisonFormula f) {
		super();
		
		this.addAll(new AllQDecls(f.left()));
		this.addAll(new AllQDecls(f.right()));
	}
	
	public AllQDecls(Decl f) {
		super();
		
		this.addAll(new AllQDecls(f.expression()));
		this.addAll(new AllQDecls(f.variable()));
	}
	
	public AllQDecls(Expression exp) {
		super();
		
		if (exp instanceof UnaryExpression) {
			UnaryExpression e = (UnaryExpression)exp;
			this.addAll(new AllQDecls(e.expression()));
		}
		else if (exp instanceof BinaryExpression) {
			BinaryExpression e = (BinaryExpression)exp;
			this.addAll(new AllQDecls(e.left()));
			this.addAll(new AllQDecls(e.right()));
		}
		else if (exp instanceof NaryExpression) {
			NaryExpression e = (NaryExpression)exp;
			for (Expression child : e) {
				this.addAll(new AllQDecls(child));
			}
		}
		else if (exp instanceof Comprehension) {
			Comprehension e = (Comprehension)exp;
			for (Decl child : e.decls()) {
				this.add(child.variable());
			}
		}
		else if (exp instanceof IfExpression) {
			IfExpression e = (IfExpression)exp;
			this.addAll(new AllQDecls(e.thenExpr()));
			this.addAll(new AllQDecls(e.elseExpr()));
		}
		else if (exp instanceof ProjectExpression) {
			ProjectExpression e = (ProjectExpression)exp;
			this.addAll(new AllQDecls(e.expression()));
		}
		else if (exp instanceof IntToExprCast) {
			IntToExprCast e = (IntToExprCast)exp;
		}
		else if (exp instanceof LeafExpression) {
			if (exp instanceof ConstantExpression) {
				ConstantExpression e = (ConstantExpression)exp;
			} 
			else if (exp instanceof Relation) {
				Relation e = (Relation)exp;
			}
			else if (exp instanceof Variable) {
				Variable var = (Variable)exp;
				if (!Analyzer.translation.skolemRelations.containsKey(var) && Analyzer.initialAnalysis.allDecls.containsKey(var)) { 
					this.add(var);
				}
			}
		}
	}
	
	public AllQDecls(IntExpression exp) {
		super();
		
		if (exp instanceof UnaryIntExpression) {
			UnaryIntExpression e = (UnaryIntExpression)exp;
			this.addAll(new AllQDecls(e.intExpr()));
		} else if (exp instanceof BinaryIntExpression) {
			BinaryIntExpression e = (BinaryIntExpression)exp;
			this.addAll(new AllQDecls(e.left()));
			this.addAll(new AllQDecls(e.right()));
		} else if (exp instanceof NaryIntExpression) {
			NaryIntExpression e = (NaryIntExpression)exp;
			for (IntExpression child : e) this.addAll(new AllQDecls(child));
		} else if (exp instanceof SumExpression) {
			SumExpression e = (SumExpression)exp;
			// TODO
		} else if (exp instanceof IfIntExpression) {
			IfIntExpression e = (IfIntExpression)exp;
			this.addAll(new AllQDecls(e.thenExpr()));
			this.addAll(new AllQDecls(e.elseExpr()));
		} else if (exp instanceof ExprToIntCast) {
			ExprToIntCast e = (ExprToIntCast)exp;
			this.addAll(new AllQDecls(e.expression()));
		} else if (exp instanceof IntConstant) {
			IntConstant e = (IntConstant)exp;
		} 
	}
}
